(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
0(1(0(x1))) → 0(2(1(0(x1))))
0(1(1(x1))) → 0(3(1(4(1(x1)))))
0(1(1(x1))) → 0(5(1(3(2(5(1(x1)))))))
0(1(1(x1))) → 3(5(5(1(0(2(1(x1)))))))
0(1(4(x1))) → 0(5(1(4(5(x1)))))
4(0(1(x1))) → 3(5(1(4(1(2(0(x1)))))))
0(0(1(1(x1)))) → 2(0(5(1(4(1(0(x1)))))))
0(0(3(4(x1)))) → 0(3(2(1(4(5(5(0(x1))))))))
0(1(1(0(x1)))) → 2(1(0(3(1(0(x1))))))
0(1(1(4(x1)))) → 3(1(4(1(0(3(5(x1)))))))
0(1(3(0(x1)))) → 0(0(3(2(1(x1)))))
0(1(3(4(x1)))) → 3(1(4(2(5(0(5(x1)))))))
0(1(4(0(x1)))) → 0(5(0(4(1(3(1(x1)))))))
0(3(4(1(x1)))) → 4(3(0(3(1(x1)))))
2(0(1(0(x1)))) → 2(0(5(1(0(x1)))))
2(0(1(1(x1)))) → 2(0(2(1(3(1(x1))))))
2(3(1(1(x1)))) → 2(3(1(4(1(x1)))))
2(3(1(1(x1)))) → 3(1(3(2(1(x1)))))
2(4(1(1(x1)))) → 2(4(2(1(4(1(x1))))))
3(0(1(0(x1)))) → 3(1(2(2(0(0(x1))))))
3(3(1(1(x1)))) → 5(3(5(1(3(2(2(1(x1))))))))
3(4(0(1(x1)))) → 0(3(1(4(1(x1)))))
3(4(1(1(x1)))) → 3(4(1(3(1(x1)))))
3(4(5(4(x1)))) → 5(1(4(1(4(5(3(x1)))))))
4(0(0(1(x1)))) → 4(0(0(3(1(x1)))))
4(3(0(1(x1)))) → 3(5(0(4(2(1(x1))))))
4(3(0(1(x1)))) → 3(1(4(2(5(5(2(0(x1))))))))
4(3(1(1(x1)))) → 4(3(1(3(1(x1)))))
0(0(0(1(1(x1))))) → 0(0(0(3(5(1(1(x1)))))))
0(0(0(3(4(x1))))) → 0(0(3(1(0(4(5(x1)))))))
0(0(1(3(0(x1))))) → 0(3(1(0(5(0(5(x1)))))))
0(0(2(0(1(x1))))) → 0(0(0(3(2(1(x1))))))
0(1(1(3(4(x1))))) → 0(5(4(1(3(1(x1))))))
0(1(1(3(4(x1))))) → 4(1(0(3(5(5(2(1(x1))))))))
0(1(2(5(4(x1))))) → 3(2(1(0(4(5(x1))))))
0(5(5(0(1(x1))))) → 0(5(5(5(1(0(2(x1)))))))
2(0(1(4(1(x1))))) → 5(5(1(0(4(2(1(x1)))))))
2(2(3(1(1(x1))))) → 3(2(2(1(4(1(x1))))))
2(3(4(1(1(x1))))) → 2(1(3(5(4(1(x1))))))
2(4(4(0(1(x1))))) → 4(5(2(1(4(5(5(0(x1))))))))
3(0(4(0(1(x1))))) → 4(0(3(1(2(2(0(x1)))))))
3(2(3(1(1(x1))))) → 3(5(1(3(2(1(x1))))))
3(3(0(1(0(x1))))) → 3(2(5(2(1(3(0(0(x1))))))))
3(3(4(0(1(x1))))) → 3(5(0(3(1(2(4(1(x1))))))))
3(4(2(0(1(x1))))) → 0(3(1(4(2(1(x1))))))
3(4(3(0(1(x1))))) → 0(3(1(3(5(4(x1))))))
4(0(1(1(4(x1))))) → 4(0(1(3(1(4(5(5(x1))))))))
4(3(2(0(1(x1))))) → 3(1(2(2(4(0(x1))))))
4(3(4(1(1(x1))))) → 3(1(4(1(4(2(x1))))))
0(0(2(1(1(1(x1)))))) → 5(1(0(4(1(0(2(1(x1))))))))
0(1(1(2(5(4(x1)))))) → 0(2(3(1(4(5(1(x1)))))))
0(1(5(1(4(0(x1)))))) → 0(5(1(4(2(1(0(5(x1))))))))
0(2(5(3(1(1(x1)))))) → 3(0(2(1(3(5(1(x1)))))))
0(3(0(5(4(1(x1)))))) → 3(2(1(0(4(5(0(x1)))))))
0(5(5(3(3(4(x1)))))) → 3(5(5(0(4(5(5(3(x1))))))))
2(0(4(4(1(1(x1)))))) → 4(0(0(2(1(4(5(1(x1))))))))
2(2(3(1(0(1(x1)))))) → 0(2(5(2(1(3(1(x1)))))))
2(3(0(1(1(1(x1)))))) → 3(1(4(1(0(2(5(1(x1))))))))
2(3(2(3(0(1(x1)))))) → 2(3(5(1(3(1(2(0(x1))))))))
2(3(4(1(0(1(x1)))))) → 3(3(2(1(4(5(1(0(x1))))))))
3(0(1(4(1(1(x1)))))) → 3(1(2(2(1(4(1(0(x1))))))))
3(0(5(2(5(4(x1)))))) → 4(3(5(2(1(0(5(x1)))))))
3(3(0(2(5(0(x1)))))) → 3(2(5(0(0(3(1(x1)))))))
3(3(1(4(0(0(x1)))))) → 4(0(3(1(3(5(0(x1)))))))
3(4(1(2(5(0(x1)))))) → 4(4(5(0(3(2(1(x1)))))))
3(4(2(2(0(1(x1)))))) → 3(2(2(3(1(4(5(0(x1))))))))
3(4(5(3(0(1(x1)))))) → 5(1(0(3(2(5(3(4(x1))))))))
4(0(1(3(0(1(x1)))))) → 0(3(1(4(1(0(3(x1)))))))
4(0(3(4(1(1(x1)))))) → 0(1(4(3(1(4(5(4(x1))))))))
4(2(0(5(1(1(x1)))))) → 3(5(0(2(1(4(2(1(x1))))))))
4(3(0(1(0(4(x1)))))) → 2(0(4(5(1(3(0(4(x1))))))))
0(1(2(3(4(0(1(x1))))))) → 2(0(4(5(1(3(1(0(x1))))))))
2(3(4(5(4(1(1(x1))))))) → 2(1(3(4(3(5(4(1(x1))))))))
2(4(0(2(1(0(1(x1))))))) → 0(2(2(1(4(5(0(1(x1))))))))
2(4(3(4(2(1(1(x1))))))) → 2(5(1(2(4(4(3(1(x1))))))))
2(4(5(0(3(0(1(x1))))))) → 2(0(0(4(3(2(5(1(x1))))))))
3(0(0(4(0(1(1(x1))))))) → 3(2(1(0(0(0(4(1(x1))))))))
3(2(4(5(1(0(1(x1))))))) → 1(3(5(2(1(4(1(0(x1))))))))
4(0(3(2(0(0(1(x1))))))) → 0(0(5(1(4(2(3(0(x1))))))))
4(3(0(5(0(1(4(x1))))))) → 5(0(4(1(0(3(1(4(x1))))))))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(0(z0))) → 0(2(1(0(z0))))
0(1(1(z0))) → 0(3(1(4(1(z0)))))
0(1(1(z0))) → 0(5(1(3(2(5(1(z0)))))))
0(1(1(z0))) → 3(5(5(1(0(2(1(z0)))))))
0(1(4(z0))) → 0(5(1(4(5(z0)))))
0(0(1(1(z0)))) → 2(0(5(1(4(1(0(z0)))))))
0(0(3(4(z0)))) → 0(3(2(1(4(5(5(0(z0))))))))
0(1(1(0(z0)))) → 2(1(0(3(1(0(z0))))))
0(1(1(4(z0)))) → 3(1(4(1(0(3(5(z0)))))))
0(1(3(0(z0)))) → 0(0(3(2(1(z0)))))
0(1(3(4(z0)))) → 3(1(4(2(5(0(5(z0)))))))
0(1(4(0(z0)))) → 0(5(0(4(1(3(1(z0)))))))
0(3(4(1(z0)))) → 4(3(0(3(1(z0)))))
0(0(0(1(1(z0))))) → 0(0(0(3(5(1(1(z0)))))))
0(0(0(3(4(z0))))) → 0(0(3(1(0(4(5(z0)))))))
0(0(1(3(0(z0))))) → 0(3(1(0(5(0(5(z0)))))))
0(0(2(0(1(z0))))) → 0(0(0(3(2(1(z0))))))
0(1(1(3(4(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(3(4(z0))))) → 4(1(0(3(5(5(2(1(z0))))))))
0(1(2(5(4(z0))))) → 3(2(1(0(4(5(z0))))))
0(5(5(0(1(z0))))) → 0(5(5(5(1(0(2(z0)))))))
0(0(2(1(1(1(z0)))))) → 5(1(0(4(1(0(2(1(z0))))))))
0(1(1(2(5(4(z0)))))) → 0(2(3(1(4(5(1(z0)))))))
0(1(5(1(4(0(z0)))))) → 0(5(1(4(2(1(0(5(z0))))))))
0(2(5(3(1(1(z0)))))) → 3(0(2(1(3(5(1(z0)))))))
0(3(0(5(4(1(z0)))))) → 3(2(1(0(4(5(0(z0)))))))
0(5(5(3(3(4(z0)))))) → 3(5(5(0(4(5(5(3(z0))))))))
0(1(2(3(4(0(1(z0))))))) → 2(0(4(5(1(3(1(0(z0))))))))
4(0(1(z0))) → 3(5(1(4(1(2(0(z0)))))))
4(0(0(1(z0)))) → 4(0(0(3(1(z0)))))
4(3(0(1(z0)))) → 3(5(0(4(2(1(z0))))))
4(3(0(1(z0)))) → 3(1(4(2(5(5(2(0(z0))))))))
4(3(1(1(z0)))) → 4(3(1(3(1(z0)))))
4(0(1(1(4(z0))))) → 4(0(1(3(1(4(5(5(z0))))))))
4(3(2(0(1(z0))))) → 3(1(2(2(4(0(z0))))))
4(3(4(1(1(z0))))) → 3(1(4(1(4(2(z0))))))
4(0(1(3(0(1(z0)))))) → 0(3(1(4(1(0(3(z0)))))))
4(0(3(4(1(1(z0)))))) → 0(1(4(3(1(4(5(4(z0))))))))
4(2(0(5(1(1(z0)))))) → 3(5(0(2(1(4(2(1(z0))))))))
4(3(0(1(0(4(z0)))))) → 2(0(4(5(1(3(0(4(z0))))))))
4(0(3(2(0(0(1(z0))))))) → 0(0(5(1(4(2(3(0(z0))))))))
4(3(0(5(0(1(4(z0))))))) → 5(0(4(1(0(3(1(4(z0))))))))
2(0(1(0(z0)))) → 2(0(5(1(0(z0)))))
2(0(1(1(z0)))) → 2(0(2(1(3(1(z0))))))
2(3(1(1(z0)))) → 2(3(1(4(1(z0)))))
2(3(1(1(z0)))) → 3(1(3(2(1(z0)))))
2(4(1(1(z0)))) → 2(4(2(1(4(1(z0))))))
2(0(1(4(1(z0))))) → 5(5(1(0(4(2(1(z0)))))))
2(2(3(1(1(z0))))) → 3(2(2(1(4(1(z0))))))
2(3(4(1(1(z0))))) → 2(1(3(5(4(1(z0))))))
2(4(4(0(1(z0))))) → 4(5(2(1(4(5(5(0(z0))))))))
2(0(4(4(1(1(z0)))))) → 4(0(0(2(1(4(5(1(z0))))))))
2(2(3(1(0(1(z0)))))) → 0(2(5(2(1(3(1(z0)))))))
2(3(0(1(1(1(z0)))))) → 3(1(4(1(0(2(5(1(z0))))))))
2(3(2(3(0(1(z0)))))) → 2(3(5(1(3(1(2(0(z0))))))))
2(3(4(1(0(1(z0)))))) → 3(3(2(1(4(5(1(0(z0))))))))
2(3(4(5(4(1(1(z0))))))) → 2(1(3(4(3(5(4(1(z0))))))))
2(4(0(2(1(0(1(z0))))))) → 0(2(2(1(4(5(0(1(z0))))))))
2(4(3(4(2(1(1(z0))))))) → 2(5(1(2(4(4(3(1(z0))))))))
2(4(5(0(3(0(1(z0))))))) → 2(0(0(4(3(2(5(1(z0))))))))
3(0(1(0(z0)))) → 3(1(2(2(0(0(z0))))))
3(3(1(1(z0)))) → 5(3(5(1(3(2(2(1(z0))))))))
3(4(0(1(z0)))) → 0(3(1(4(1(z0)))))
3(4(1(1(z0)))) → 3(4(1(3(1(z0)))))
3(4(5(4(z0)))) → 5(1(4(1(4(5(3(z0)))))))
3(0(4(0(1(z0))))) → 4(0(3(1(2(2(0(z0)))))))
3(2(3(1(1(z0))))) → 3(5(1(3(2(1(z0))))))
3(3(0(1(0(z0))))) → 3(2(5(2(1(3(0(0(z0))))))))
3(3(4(0(1(z0))))) → 3(5(0(3(1(2(4(1(z0))))))))
3(4(2(0(1(z0))))) → 0(3(1(4(2(1(z0))))))
3(4(3(0(1(z0))))) → 0(3(1(3(5(4(z0))))))
3(0(1(4(1(1(z0)))))) → 3(1(2(2(1(4(1(0(z0))))))))
3(0(5(2(5(4(z0)))))) → 4(3(5(2(1(0(5(z0)))))))
3(3(0(2(5(0(z0)))))) → 3(2(5(0(0(3(1(z0)))))))
3(3(1(4(0(0(z0)))))) → 4(0(3(1(3(5(0(z0)))))))
3(4(1(2(5(0(z0)))))) → 4(4(5(0(3(2(1(z0)))))))
3(4(2(2(0(1(z0)))))) → 3(2(2(3(1(4(5(0(z0))))))))
3(4(5(3(0(1(z0)))))) → 5(1(0(3(2(5(3(4(z0))))))))
3(0(0(4(0(1(1(z0))))))) → 3(2(1(0(0(0(4(1(z0))))))))
3(2(4(5(1(0(1(z0))))))) → 1(3(5(2(1(4(1(0(z0))))))))
Tuples:
0'(1(0(z0))) → c(0'(2(1(0(z0)))), 2'(1(0(z0))), 0'(z0))
0'(1(1(z0))) → c1(0'(3(1(4(1(z0))))), 3'(1(4(1(z0)))), 4'(1(z0)))
0'(1(1(z0))) → c2(0'(5(1(3(2(5(1(z0))))))), 3'(2(5(1(z0)))), 2'(5(1(z0))))
0'(1(1(z0))) → c3(3'(5(5(1(0(2(1(z0))))))), 0'(2(1(z0))), 2'(1(z0)))
0'(1(4(z0))) → c4(0'(5(1(4(5(z0))))), 4'(5(z0)))
0'(0(1(1(z0)))) → c5(2'(0(5(1(4(1(0(z0))))))), 0'(5(1(4(1(0(z0)))))), 4'(1(0(z0))), 0'(z0))
0'(0(3(4(z0)))) → c6(0'(3(2(1(4(5(5(0(z0)))))))), 3'(2(1(4(5(5(0(z0))))))), 2'(1(4(5(5(0(z0)))))), 4'(5(5(0(z0)))), 0'(z0))
0'(1(1(0(z0)))) → c7(2'(1(0(3(1(0(z0)))))), 0'(3(1(0(z0)))), 3'(1(0(z0))), 0'(z0))
0'(1(1(4(z0)))) → c8(3'(1(4(1(0(3(5(z0))))))), 4'(1(0(3(5(z0))))), 0'(3(5(z0))), 3'(5(z0)))
0'(1(3(0(z0)))) → c9(0'(0(3(2(1(z0))))), 0'(3(2(1(z0)))), 3'(2(1(z0))), 2'(1(z0)))
0'(1(3(4(z0)))) → c10(3'(1(4(2(5(0(5(z0))))))), 4'(2(5(0(5(z0))))), 2'(5(0(5(z0)))), 0'(5(z0)))
0'(1(4(0(z0)))) → c11(0'(5(0(4(1(3(1(z0))))))), 0'(4(1(3(1(z0))))), 4'(1(3(1(z0)))), 3'(1(z0)))
0'(3(4(1(z0)))) → c12(4'(3(0(3(1(z0))))), 3'(0(3(1(z0)))), 0'(3(1(z0))), 3'(1(z0)))
0'(0(0(1(1(z0))))) → c13(0'(0(0(3(5(1(1(z0))))))), 0'(0(3(5(1(1(z0)))))), 0'(3(5(1(1(z0))))), 3'(5(1(1(z0)))))
0'(0(0(3(4(z0))))) → c14(0'(0(3(1(0(4(5(z0))))))), 0'(3(1(0(4(5(z0)))))), 3'(1(0(4(5(z0))))), 0'(4(5(z0))), 4'(5(z0)))
0'(0(1(3(0(z0))))) → c15(0'(3(1(0(5(0(5(z0))))))), 3'(1(0(5(0(5(z0)))))), 0'(5(0(5(z0)))), 0'(5(z0)))
0'(0(2(0(1(z0))))) → c16(0'(0(0(3(2(1(z0)))))), 0'(0(3(2(1(z0))))), 0'(3(2(1(z0)))), 3'(2(1(z0))), 2'(1(z0)))
0'(1(1(3(4(z0))))) → c17(0'(5(4(1(3(1(z0)))))), 4'(1(3(1(z0)))), 3'(1(z0)))
0'(1(1(3(4(z0))))) → c18(4'(1(0(3(5(5(2(1(z0)))))))), 0'(3(5(5(2(1(z0)))))), 3'(5(5(2(1(z0))))), 2'(1(z0)))
0'(1(2(5(4(z0))))) → c19(3'(2(1(0(4(5(z0)))))), 2'(1(0(4(5(z0))))), 0'(4(5(z0))), 4'(5(z0)))
0'(5(5(0(1(z0))))) → c20(0'(5(5(5(1(0(2(z0))))))), 0'(2(z0)), 2'(z0))
0'(0(2(1(1(1(z0)))))) → c21(0'(4(1(0(2(1(z0)))))), 4'(1(0(2(1(z0))))), 0'(2(1(z0))), 2'(1(z0)))
0'(1(1(2(5(4(z0)))))) → c22(0'(2(3(1(4(5(1(z0))))))), 2'(3(1(4(5(1(z0)))))), 3'(1(4(5(1(z0))))), 4'(5(1(z0))))
0'(1(5(1(4(0(z0)))))) → c23(0'(5(1(4(2(1(0(5(z0)))))))), 4'(2(1(0(5(z0))))), 2'(1(0(5(z0)))), 0'(5(z0)))
0'(2(5(3(1(1(z0)))))) → c24(3'(0(2(1(3(5(1(z0))))))), 0'(2(1(3(5(1(z0)))))), 2'(1(3(5(1(z0))))), 3'(5(1(z0))))
0'(3(0(5(4(1(z0)))))) → c25(3'(2(1(0(4(5(0(z0))))))), 2'(1(0(4(5(0(z0)))))), 0'(4(5(0(z0)))), 4'(5(0(z0))), 0'(z0))
0'(5(5(3(3(4(z0)))))) → c26(3'(5(5(0(4(5(5(3(z0)))))))), 0'(4(5(5(3(z0))))), 4'(5(5(3(z0)))), 3'(z0))
0'(1(2(3(4(0(1(z0))))))) → c27(2'(0(4(5(1(3(1(0(z0)))))))), 0'(4(5(1(3(1(0(z0))))))), 4'(5(1(3(1(0(z0)))))), 3'(1(0(z0))), 0'(z0))
4'(0(1(z0))) → c28(3'(5(1(4(1(2(0(z0))))))), 4'(1(2(0(z0)))), 2'(0(z0)), 0'(z0))
4'(0(0(1(z0)))) → c29(4'(0(0(3(1(z0))))), 0'(0(3(1(z0)))), 0'(3(1(z0))), 3'(1(z0)))
4'(3(0(1(z0)))) → c30(3'(5(0(4(2(1(z0)))))), 0'(4(2(1(z0)))), 4'(2(1(z0))), 2'(1(z0)))
4'(3(0(1(z0)))) → c31(3'(1(4(2(5(5(2(0(z0)))))))), 4'(2(5(5(2(0(z0)))))), 2'(5(5(2(0(z0))))), 2'(0(z0)), 0'(z0))
4'(3(1(1(z0)))) → c32(4'(3(1(3(1(z0))))), 3'(1(3(1(z0)))), 3'(1(z0)))
4'(0(1(1(4(z0))))) → c33(4'(0(1(3(1(4(5(5(z0)))))))), 0'(1(3(1(4(5(5(z0))))))), 3'(1(4(5(5(z0))))), 4'(5(5(z0))))
4'(3(2(0(1(z0))))) → c34(3'(1(2(2(4(0(z0)))))), 2'(2(4(0(z0)))), 2'(4(0(z0))), 4'(0(z0)), 0'(z0))
4'(3(4(1(1(z0))))) → c35(3'(1(4(1(4(2(z0)))))), 4'(1(4(2(z0)))), 4'(2(z0)), 2'(z0))
4'(0(1(3(0(1(z0)))))) → c36(0'(3(1(4(1(0(3(z0))))))), 3'(1(4(1(0(3(z0)))))), 4'(1(0(3(z0)))), 0'(3(z0)), 3'(z0))
4'(0(3(4(1(1(z0)))))) → c37(0'(1(4(3(1(4(5(4(z0)))))))), 4'(3(1(4(5(4(z0)))))), 3'(1(4(5(4(z0))))), 4'(5(4(z0))), 4'(z0))
4'(2(0(5(1(1(z0)))))) → c38(3'(5(0(2(1(4(2(1(z0)))))))), 0'(2(1(4(2(1(z0)))))), 2'(1(4(2(1(z0))))), 4'(2(1(z0))), 2'(1(z0)))
4'(3(0(1(0(4(z0)))))) → c39(2'(0(4(5(1(3(0(4(z0)))))))), 0'(4(5(1(3(0(4(z0))))))), 4'(5(1(3(0(4(z0)))))), 3'(0(4(z0))), 0'(4(z0)), 4'(z0))
4'(0(3(2(0(0(1(z0))))))) → c40(0'(0(5(1(4(2(3(0(z0)))))))), 0'(5(1(4(2(3(0(z0))))))), 4'(2(3(0(z0)))), 2'(3(0(z0))), 3'(0(z0)), 0'(z0))
4'(3(0(5(0(1(4(z0))))))) → c41(0'(4(1(0(3(1(4(z0))))))), 4'(1(0(3(1(4(z0)))))), 0'(3(1(4(z0)))), 3'(1(4(z0))), 4'(z0))
2'(0(1(0(z0)))) → c42(2'(0(5(1(0(z0))))), 0'(5(1(0(z0)))), 0'(z0))
2'(0(1(1(z0)))) → c43(2'(0(2(1(3(1(z0)))))), 0'(2(1(3(1(z0))))), 2'(1(3(1(z0)))), 3'(1(z0)))
2'(3(1(1(z0)))) → c44(2'(3(1(4(1(z0))))), 3'(1(4(1(z0)))), 4'(1(z0)))
2'(3(1(1(z0)))) → c45(3'(1(3(2(1(z0))))), 3'(2(1(z0))), 2'(1(z0)))
2'(4(1(1(z0)))) → c46(2'(4(2(1(4(1(z0)))))), 4'(2(1(4(1(z0))))), 2'(1(4(1(z0)))), 4'(1(z0)))
2'(0(1(4(1(z0))))) → c47(0'(4(2(1(z0)))), 4'(2(1(z0))), 2'(1(z0)))
2'(2(3(1(1(z0))))) → c48(3'(2(2(1(4(1(z0)))))), 2'(2(1(4(1(z0))))), 2'(1(4(1(z0)))), 4'(1(z0)))
2'(3(4(1(1(z0))))) → c49(2'(1(3(5(4(1(z0)))))), 3'(5(4(1(z0)))), 4'(1(z0)))
2'(4(4(0(1(z0))))) → c50(4'(5(2(1(4(5(5(0(z0)))))))), 2'(1(4(5(5(0(z0)))))), 4'(5(5(0(z0)))), 0'(z0))
2'(0(4(4(1(1(z0)))))) → c51(4'(0(0(2(1(4(5(1(z0)))))))), 0'(0(2(1(4(5(1(z0))))))), 0'(2(1(4(5(1(z0)))))), 2'(1(4(5(1(z0))))), 4'(5(1(z0))))
2'(2(3(1(0(1(z0)))))) → c52(0'(2(5(2(1(3(1(z0))))))), 2'(5(2(1(3(1(z0)))))), 2'(1(3(1(z0)))), 3'(1(z0)))
2'(3(0(1(1(1(z0)))))) → c53(3'(1(4(1(0(2(5(1(z0)))))))), 4'(1(0(2(5(1(z0)))))), 0'(2(5(1(z0)))), 2'(5(1(z0))))
2'(3(2(3(0(1(z0)))))) → c54(2'(3(5(1(3(1(2(0(z0)))))))), 3'(5(1(3(1(2(0(z0))))))), 3'(1(2(0(z0)))), 2'(0(z0)), 0'(z0))
2'(3(4(1(0(1(z0)))))) → c55(3'(3(2(1(4(5(1(0(z0)))))))), 3'(2(1(4(5(1(0(z0))))))), 2'(1(4(5(1(0(z0)))))), 4'(5(1(0(z0)))), 0'(z0))
2'(3(4(5(4(1(1(z0))))))) → c56(2'(1(3(4(3(5(4(1(z0)))))))), 3'(4(3(5(4(1(z0)))))), 4'(3(5(4(1(z0))))), 3'(5(4(1(z0)))), 4'(1(z0)))
2'(4(0(2(1(0(1(z0))))))) → c57(0'(2(2(1(4(5(0(1(z0)))))))), 2'(2(1(4(5(0(1(z0))))))), 2'(1(4(5(0(1(z0)))))), 4'(5(0(1(z0)))), 0'(1(z0)))
2'(4(3(4(2(1(1(z0))))))) → c58(2'(5(1(2(4(4(3(1(z0)))))))), 2'(4(4(3(1(z0))))), 4'(4(3(1(z0)))), 4'(3(1(z0))), 3'(1(z0)))
2'(4(5(0(3(0(1(z0))))))) → c59(2'(0(0(4(3(2(5(1(z0)))))))), 0'(0(4(3(2(5(1(z0))))))), 0'(4(3(2(5(1(z0)))))), 4'(3(2(5(1(z0))))), 3'(2(5(1(z0)))), 2'(5(1(z0))))
3'(0(1(0(z0)))) → c60(3'(1(2(2(0(0(z0)))))), 2'(2(0(0(z0)))), 2'(0(0(z0))), 0'(0(z0)), 0'(z0))
3'(3(1(1(z0)))) → c61(3'(5(1(3(2(2(1(z0))))))), 3'(2(2(1(z0)))), 2'(2(1(z0))), 2'(1(z0)))
3'(4(0(1(z0)))) → c62(0'(3(1(4(1(z0))))), 3'(1(4(1(z0)))), 4'(1(z0)))
3'(4(1(1(z0)))) → c63(3'(4(1(3(1(z0))))), 4'(1(3(1(z0)))), 3'(1(z0)))
3'(4(5(4(z0)))) → c64(4'(1(4(5(3(z0))))), 4'(5(3(z0))), 3'(z0))
3'(0(4(0(1(z0))))) → c65(4'(0(3(1(2(2(0(z0))))))), 0'(3(1(2(2(0(z0)))))), 3'(1(2(2(0(z0))))), 2'(2(0(z0))), 2'(0(z0)), 0'(z0))
3'(2(3(1(1(z0))))) → c66(3'(5(1(3(2(1(z0)))))), 3'(2(1(z0))), 2'(1(z0)))
3'(3(0(1(0(z0))))) → c67(3'(2(5(2(1(3(0(0(z0)))))))), 2'(5(2(1(3(0(0(z0))))))), 2'(1(3(0(0(z0))))), 3'(0(0(z0))), 0'(0(z0)), 0'(z0))
3'(3(4(0(1(z0))))) → c68(3'(5(0(3(1(2(4(1(z0)))))))), 0'(3(1(2(4(1(z0)))))), 3'(1(2(4(1(z0))))), 2'(4(1(z0))), 4'(1(z0)))
3'(4(2(0(1(z0))))) → c69(0'(3(1(4(2(1(z0)))))), 3'(1(4(2(1(z0))))), 4'(2(1(z0))), 2'(1(z0)))
3'(4(3(0(1(z0))))) → c70(0'(3(1(3(5(4(z0)))))), 3'(1(3(5(4(z0))))), 3'(5(4(z0))), 4'(z0))
3'(0(1(4(1(1(z0)))))) → c71(3'(1(2(2(1(4(1(0(z0)))))))), 2'(2(1(4(1(0(z0)))))), 2'(1(4(1(0(z0))))), 4'(1(0(z0))), 0'(z0))
3'(0(5(2(5(4(z0)))))) → c72(4'(3(5(2(1(0(5(z0))))))), 3'(5(2(1(0(5(z0)))))), 2'(1(0(5(z0)))), 0'(5(z0)))
3'(3(0(2(5(0(z0)))))) → c73(3'(2(5(0(0(3(1(z0))))))), 2'(5(0(0(3(1(z0)))))), 0'(0(3(1(z0)))), 0'(3(1(z0))), 3'(1(z0)))
3'(3(1(4(0(0(z0)))))) → c74(4'(0(3(1(3(5(0(z0))))))), 0'(3(1(3(5(0(z0)))))), 3'(1(3(5(0(z0))))), 3'(5(0(z0))), 0'(z0))
3'(4(1(2(5(0(z0)))))) → c75(4'(4(5(0(3(2(1(z0))))))), 4'(5(0(3(2(1(z0)))))), 0'(3(2(1(z0)))), 3'(2(1(z0))), 2'(1(z0)))
3'(4(2(2(0(1(z0)))))) → c76(3'(2(2(3(1(4(5(0(z0)))))))), 2'(2(3(1(4(5(0(z0))))))), 2'(3(1(4(5(0(z0)))))), 3'(1(4(5(0(z0))))), 4'(5(0(z0))), 0'(z0))
3'(4(5(3(0(1(z0)))))) → c77(0'(3(2(5(3(4(z0)))))), 3'(2(5(3(4(z0))))), 2'(5(3(4(z0)))), 3'(4(z0)), 4'(z0))
3'(0(0(4(0(1(1(z0))))))) → c78(3'(2(1(0(0(0(4(1(z0)))))))), 2'(1(0(0(0(4(1(z0))))))), 0'(0(0(4(1(z0))))), 0'(0(4(1(z0)))), 0'(4(1(z0))), 4'(1(z0)))
3'(2(4(5(1(0(1(z0))))))) → c79(3'(5(2(1(4(1(0(z0))))))), 2'(1(4(1(0(z0))))), 4'(1(0(z0))), 0'(z0))
S tuples:
0'(1(0(z0))) → c(0'(2(1(0(z0)))), 2'(1(0(z0))), 0'(z0))
0'(1(1(z0))) → c1(0'(3(1(4(1(z0))))), 3'(1(4(1(z0)))), 4'(1(z0)))
0'(1(1(z0))) → c2(0'(5(1(3(2(5(1(z0))))))), 3'(2(5(1(z0)))), 2'(5(1(z0))))
0'(1(1(z0))) → c3(3'(5(5(1(0(2(1(z0))))))), 0'(2(1(z0))), 2'(1(z0)))
0'(1(4(z0))) → c4(0'(5(1(4(5(z0))))), 4'(5(z0)))
0'(0(1(1(z0)))) → c5(2'(0(5(1(4(1(0(z0))))))), 0'(5(1(4(1(0(z0)))))), 4'(1(0(z0))), 0'(z0))
0'(0(3(4(z0)))) → c6(0'(3(2(1(4(5(5(0(z0)))))))), 3'(2(1(4(5(5(0(z0))))))), 2'(1(4(5(5(0(z0)))))), 4'(5(5(0(z0)))), 0'(z0))
0'(1(1(0(z0)))) → c7(2'(1(0(3(1(0(z0)))))), 0'(3(1(0(z0)))), 3'(1(0(z0))), 0'(z0))
0'(1(1(4(z0)))) → c8(3'(1(4(1(0(3(5(z0))))))), 4'(1(0(3(5(z0))))), 0'(3(5(z0))), 3'(5(z0)))
0'(1(3(0(z0)))) → c9(0'(0(3(2(1(z0))))), 0'(3(2(1(z0)))), 3'(2(1(z0))), 2'(1(z0)))
0'(1(3(4(z0)))) → c10(3'(1(4(2(5(0(5(z0))))))), 4'(2(5(0(5(z0))))), 2'(5(0(5(z0)))), 0'(5(z0)))
0'(1(4(0(z0)))) → c11(0'(5(0(4(1(3(1(z0))))))), 0'(4(1(3(1(z0))))), 4'(1(3(1(z0)))), 3'(1(z0)))
0'(3(4(1(z0)))) → c12(4'(3(0(3(1(z0))))), 3'(0(3(1(z0)))), 0'(3(1(z0))), 3'(1(z0)))
0'(0(0(1(1(z0))))) → c13(0'(0(0(3(5(1(1(z0))))))), 0'(0(3(5(1(1(z0)))))), 0'(3(5(1(1(z0))))), 3'(5(1(1(z0)))))
0'(0(0(3(4(z0))))) → c14(0'(0(3(1(0(4(5(z0))))))), 0'(3(1(0(4(5(z0)))))), 3'(1(0(4(5(z0))))), 0'(4(5(z0))), 4'(5(z0)))
0'(0(1(3(0(z0))))) → c15(0'(3(1(0(5(0(5(z0))))))), 3'(1(0(5(0(5(z0)))))), 0'(5(0(5(z0)))), 0'(5(z0)))
0'(0(2(0(1(z0))))) → c16(0'(0(0(3(2(1(z0)))))), 0'(0(3(2(1(z0))))), 0'(3(2(1(z0)))), 3'(2(1(z0))), 2'(1(z0)))
0'(1(1(3(4(z0))))) → c17(0'(5(4(1(3(1(z0)))))), 4'(1(3(1(z0)))), 3'(1(z0)))
0'(1(1(3(4(z0))))) → c18(4'(1(0(3(5(5(2(1(z0)))))))), 0'(3(5(5(2(1(z0)))))), 3'(5(5(2(1(z0))))), 2'(1(z0)))
0'(1(2(5(4(z0))))) → c19(3'(2(1(0(4(5(z0)))))), 2'(1(0(4(5(z0))))), 0'(4(5(z0))), 4'(5(z0)))
0'(5(5(0(1(z0))))) → c20(0'(5(5(5(1(0(2(z0))))))), 0'(2(z0)), 2'(z0))
0'(0(2(1(1(1(z0)))))) → c21(0'(4(1(0(2(1(z0)))))), 4'(1(0(2(1(z0))))), 0'(2(1(z0))), 2'(1(z0)))
0'(1(1(2(5(4(z0)))))) → c22(0'(2(3(1(4(5(1(z0))))))), 2'(3(1(4(5(1(z0)))))), 3'(1(4(5(1(z0))))), 4'(5(1(z0))))
0'(1(5(1(4(0(z0)))))) → c23(0'(5(1(4(2(1(0(5(z0)))))))), 4'(2(1(0(5(z0))))), 2'(1(0(5(z0)))), 0'(5(z0)))
0'(2(5(3(1(1(z0)))))) → c24(3'(0(2(1(3(5(1(z0))))))), 0'(2(1(3(5(1(z0)))))), 2'(1(3(5(1(z0))))), 3'(5(1(z0))))
0'(3(0(5(4(1(z0)))))) → c25(3'(2(1(0(4(5(0(z0))))))), 2'(1(0(4(5(0(z0)))))), 0'(4(5(0(z0)))), 4'(5(0(z0))), 0'(z0))
0'(5(5(3(3(4(z0)))))) → c26(3'(5(5(0(4(5(5(3(z0)))))))), 0'(4(5(5(3(z0))))), 4'(5(5(3(z0)))), 3'(z0))
0'(1(2(3(4(0(1(z0))))))) → c27(2'(0(4(5(1(3(1(0(z0)))))))), 0'(4(5(1(3(1(0(z0))))))), 4'(5(1(3(1(0(z0)))))), 3'(1(0(z0))), 0'(z0))
4'(0(1(z0))) → c28(3'(5(1(4(1(2(0(z0))))))), 4'(1(2(0(z0)))), 2'(0(z0)), 0'(z0))
4'(0(0(1(z0)))) → c29(4'(0(0(3(1(z0))))), 0'(0(3(1(z0)))), 0'(3(1(z0))), 3'(1(z0)))
4'(3(0(1(z0)))) → c30(3'(5(0(4(2(1(z0)))))), 0'(4(2(1(z0)))), 4'(2(1(z0))), 2'(1(z0)))
4'(3(0(1(z0)))) → c31(3'(1(4(2(5(5(2(0(z0)))))))), 4'(2(5(5(2(0(z0)))))), 2'(5(5(2(0(z0))))), 2'(0(z0)), 0'(z0))
4'(3(1(1(z0)))) → c32(4'(3(1(3(1(z0))))), 3'(1(3(1(z0)))), 3'(1(z0)))
4'(0(1(1(4(z0))))) → c33(4'(0(1(3(1(4(5(5(z0)))))))), 0'(1(3(1(4(5(5(z0))))))), 3'(1(4(5(5(z0))))), 4'(5(5(z0))))
4'(3(2(0(1(z0))))) → c34(3'(1(2(2(4(0(z0)))))), 2'(2(4(0(z0)))), 2'(4(0(z0))), 4'(0(z0)), 0'(z0))
4'(3(4(1(1(z0))))) → c35(3'(1(4(1(4(2(z0)))))), 4'(1(4(2(z0)))), 4'(2(z0)), 2'(z0))
4'(0(1(3(0(1(z0)))))) → c36(0'(3(1(4(1(0(3(z0))))))), 3'(1(4(1(0(3(z0)))))), 4'(1(0(3(z0)))), 0'(3(z0)), 3'(z0))
4'(0(3(4(1(1(z0)))))) → c37(0'(1(4(3(1(4(5(4(z0)))))))), 4'(3(1(4(5(4(z0)))))), 3'(1(4(5(4(z0))))), 4'(5(4(z0))), 4'(z0))
4'(2(0(5(1(1(z0)))))) → c38(3'(5(0(2(1(4(2(1(z0)))))))), 0'(2(1(4(2(1(z0)))))), 2'(1(4(2(1(z0))))), 4'(2(1(z0))), 2'(1(z0)))
4'(3(0(1(0(4(z0)))))) → c39(2'(0(4(5(1(3(0(4(z0)))))))), 0'(4(5(1(3(0(4(z0))))))), 4'(5(1(3(0(4(z0)))))), 3'(0(4(z0))), 0'(4(z0)), 4'(z0))
4'(0(3(2(0(0(1(z0))))))) → c40(0'(0(5(1(4(2(3(0(z0)))))))), 0'(5(1(4(2(3(0(z0))))))), 4'(2(3(0(z0)))), 2'(3(0(z0))), 3'(0(z0)), 0'(z0))
4'(3(0(5(0(1(4(z0))))))) → c41(0'(4(1(0(3(1(4(z0))))))), 4'(1(0(3(1(4(z0)))))), 0'(3(1(4(z0)))), 3'(1(4(z0))), 4'(z0))
2'(0(1(0(z0)))) → c42(2'(0(5(1(0(z0))))), 0'(5(1(0(z0)))), 0'(z0))
2'(0(1(1(z0)))) → c43(2'(0(2(1(3(1(z0)))))), 0'(2(1(3(1(z0))))), 2'(1(3(1(z0)))), 3'(1(z0)))
2'(3(1(1(z0)))) → c44(2'(3(1(4(1(z0))))), 3'(1(4(1(z0)))), 4'(1(z0)))
2'(3(1(1(z0)))) → c45(3'(1(3(2(1(z0))))), 3'(2(1(z0))), 2'(1(z0)))
2'(4(1(1(z0)))) → c46(2'(4(2(1(4(1(z0)))))), 4'(2(1(4(1(z0))))), 2'(1(4(1(z0)))), 4'(1(z0)))
2'(0(1(4(1(z0))))) → c47(0'(4(2(1(z0)))), 4'(2(1(z0))), 2'(1(z0)))
2'(2(3(1(1(z0))))) → c48(3'(2(2(1(4(1(z0)))))), 2'(2(1(4(1(z0))))), 2'(1(4(1(z0)))), 4'(1(z0)))
2'(3(4(1(1(z0))))) → c49(2'(1(3(5(4(1(z0)))))), 3'(5(4(1(z0)))), 4'(1(z0)))
2'(4(4(0(1(z0))))) → c50(4'(5(2(1(4(5(5(0(z0)))))))), 2'(1(4(5(5(0(z0)))))), 4'(5(5(0(z0)))), 0'(z0))
2'(0(4(4(1(1(z0)))))) → c51(4'(0(0(2(1(4(5(1(z0)))))))), 0'(0(2(1(4(5(1(z0))))))), 0'(2(1(4(5(1(z0)))))), 2'(1(4(5(1(z0))))), 4'(5(1(z0))))
2'(2(3(1(0(1(z0)))))) → c52(0'(2(5(2(1(3(1(z0))))))), 2'(5(2(1(3(1(z0)))))), 2'(1(3(1(z0)))), 3'(1(z0)))
2'(3(0(1(1(1(z0)))))) → c53(3'(1(4(1(0(2(5(1(z0)))))))), 4'(1(0(2(5(1(z0)))))), 0'(2(5(1(z0)))), 2'(5(1(z0))))
2'(3(2(3(0(1(z0)))))) → c54(2'(3(5(1(3(1(2(0(z0)))))))), 3'(5(1(3(1(2(0(z0))))))), 3'(1(2(0(z0)))), 2'(0(z0)), 0'(z0))
2'(3(4(1(0(1(z0)))))) → c55(3'(3(2(1(4(5(1(0(z0)))))))), 3'(2(1(4(5(1(0(z0))))))), 2'(1(4(5(1(0(z0)))))), 4'(5(1(0(z0)))), 0'(z0))
2'(3(4(5(4(1(1(z0))))))) → c56(2'(1(3(4(3(5(4(1(z0)))))))), 3'(4(3(5(4(1(z0)))))), 4'(3(5(4(1(z0))))), 3'(5(4(1(z0)))), 4'(1(z0)))
2'(4(0(2(1(0(1(z0))))))) → c57(0'(2(2(1(4(5(0(1(z0)))))))), 2'(2(1(4(5(0(1(z0))))))), 2'(1(4(5(0(1(z0)))))), 4'(5(0(1(z0)))), 0'(1(z0)))
2'(4(3(4(2(1(1(z0))))))) → c58(2'(5(1(2(4(4(3(1(z0)))))))), 2'(4(4(3(1(z0))))), 4'(4(3(1(z0)))), 4'(3(1(z0))), 3'(1(z0)))
2'(4(5(0(3(0(1(z0))))))) → c59(2'(0(0(4(3(2(5(1(z0)))))))), 0'(0(4(3(2(5(1(z0))))))), 0'(4(3(2(5(1(z0)))))), 4'(3(2(5(1(z0))))), 3'(2(5(1(z0)))), 2'(5(1(z0))))
3'(0(1(0(z0)))) → c60(3'(1(2(2(0(0(z0)))))), 2'(2(0(0(z0)))), 2'(0(0(z0))), 0'(0(z0)), 0'(z0))
3'(3(1(1(z0)))) → c61(3'(5(1(3(2(2(1(z0))))))), 3'(2(2(1(z0)))), 2'(2(1(z0))), 2'(1(z0)))
3'(4(0(1(z0)))) → c62(0'(3(1(4(1(z0))))), 3'(1(4(1(z0)))), 4'(1(z0)))
3'(4(1(1(z0)))) → c63(3'(4(1(3(1(z0))))), 4'(1(3(1(z0)))), 3'(1(z0)))
3'(4(5(4(z0)))) → c64(4'(1(4(5(3(z0))))), 4'(5(3(z0))), 3'(z0))
3'(0(4(0(1(z0))))) → c65(4'(0(3(1(2(2(0(z0))))))), 0'(3(1(2(2(0(z0)))))), 3'(1(2(2(0(z0))))), 2'(2(0(z0))), 2'(0(z0)), 0'(z0))
3'(2(3(1(1(z0))))) → c66(3'(5(1(3(2(1(z0)))))), 3'(2(1(z0))), 2'(1(z0)))
3'(3(0(1(0(z0))))) → c67(3'(2(5(2(1(3(0(0(z0)))))))), 2'(5(2(1(3(0(0(z0))))))), 2'(1(3(0(0(z0))))), 3'(0(0(z0))), 0'(0(z0)), 0'(z0))
3'(3(4(0(1(z0))))) → c68(3'(5(0(3(1(2(4(1(z0)))))))), 0'(3(1(2(4(1(z0)))))), 3'(1(2(4(1(z0))))), 2'(4(1(z0))), 4'(1(z0)))
3'(4(2(0(1(z0))))) → c69(0'(3(1(4(2(1(z0)))))), 3'(1(4(2(1(z0))))), 4'(2(1(z0))), 2'(1(z0)))
3'(4(3(0(1(z0))))) → c70(0'(3(1(3(5(4(z0)))))), 3'(1(3(5(4(z0))))), 3'(5(4(z0))), 4'(z0))
3'(0(1(4(1(1(z0)))))) → c71(3'(1(2(2(1(4(1(0(z0)))))))), 2'(2(1(4(1(0(z0)))))), 2'(1(4(1(0(z0))))), 4'(1(0(z0))), 0'(z0))
3'(0(5(2(5(4(z0)))))) → c72(4'(3(5(2(1(0(5(z0))))))), 3'(5(2(1(0(5(z0)))))), 2'(1(0(5(z0)))), 0'(5(z0)))
3'(3(0(2(5(0(z0)))))) → c73(3'(2(5(0(0(3(1(z0))))))), 2'(5(0(0(3(1(z0)))))), 0'(0(3(1(z0)))), 0'(3(1(z0))), 3'(1(z0)))
3'(3(1(4(0(0(z0)))))) → c74(4'(0(3(1(3(5(0(z0))))))), 0'(3(1(3(5(0(z0)))))), 3'(1(3(5(0(z0))))), 3'(5(0(z0))), 0'(z0))
3'(4(1(2(5(0(z0)))))) → c75(4'(4(5(0(3(2(1(z0))))))), 4'(5(0(3(2(1(z0)))))), 0'(3(2(1(z0)))), 3'(2(1(z0))), 2'(1(z0)))
3'(4(2(2(0(1(z0)))))) → c76(3'(2(2(3(1(4(5(0(z0)))))))), 2'(2(3(1(4(5(0(z0))))))), 2'(3(1(4(5(0(z0)))))), 3'(1(4(5(0(z0))))), 4'(5(0(z0))), 0'(z0))
3'(4(5(3(0(1(z0)))))) → c77(0'(3(2(5(3(4(z0)))))), 3'(2(5(3(4(z0))))), 2'(5(3(4(z0)))), 3'(4(z0)), 4'(z0))
3'(0(0(4(0(1(1(z0))))))) → c78(3'(2(1(0(0(0(4(1(z0)))))))), 2'(1(0(0(0(4(1(z0))))))), 0'(0(0(4(1(z0))))), 0'(0(4(1(z0)))), 0'(4(1(z0))), 4'(1(z0)))
3'(2(4(5(1(0(1(z0))))))) → c79(3'(5(2(1(4(1(0(z0))))))), 2'(1(4(1(0(z0))))), 4'(1(0(z0))), 0'(z0))
K tuples:none
Defined Rule Symbols:
0, 4, 2, 3
Defined Pair Symbols:
0', 4', 2', 3'
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c67, c68, c69, c70, c71, c72, c73, c74, c75, c76, c77, c78, c79
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
0'(1(0(z0))) → c(0'(2(1(0(z0)))), 2'(1(0(z0))), 0'(z0))
0'(1(4(z0))) → c4(0'(5(1(4(5(z0))))), 4'(5(z0)))
0'(0(1(1(z0)))) → c5(2'(0(5(1(4(1(0(z0))))))), 0'(5(1(4(1(0(z0)))))), 4'(1(0(z0))), 0'(z0))
0'(0(3(4(z0)))) → c6(0'(3(2(1(4(5(5(0(z0)))))))), 3'(2(1(4(5(5(0(z0))))))), 2'(1(4(5(5(0(z0)))))), 4'(5(5(0(z0)))), 0'(z0))
0'(1(1(0(z0)))) → c7(2'(1(0(3(1(0(z0)))))), 0'(3(1(0(z0)))), 3'(1(0(z0))), 0'(z0))
0'(1(1(4(z0)))) → c8(3'(1(4(1(0(3(5(z0))))))), 4'(1(0(3(5(z0))))), 0'(3(5(z0))), 3'(5(z0)))
0'(1(3(0(z0)))) → c9(0'(0(3(2(1(z0))))), 0'(3(2(1(z0)))), 3'(2(1(z0))), 2'(1(z0)))
0'(1(3(4(z0)))) → c10(3'(1(4(2(5(0(5(z0))))))), 4'(2(5(0(5(z0))))), 2'(5(0(5(z0)))), 0'(5(z0)))
0'(1(4(0(z0)))) → c11(0'(5(0(4(1(3(1(z0))))))), 0'(4(1(3(1(z0))))), 4'(1(3(1(z0)))), 3'(1(z0)))
0'(3(4(1(z0)))) → c12(4'(3(0(3(1(z0))))), 3'(0(3(1(z0)))), 0'(3(1(z0))), 3'(1(z0)))
0'(0(0(1(1(z0))))) → c13(0'(0(0(3(5(1(1(z0))))))), 0'(0(3(5(1(1(z0)))))), 0'(3(5(1(1(z0))))), 3'(5(1(1(z0)))))
0'(0(0(3(4(z0))))) → c14(0'(0(3(1(0(4(5(z0))))))), 0'(3(1(0(4(5(z0)))))), 3'(1(0(4(5(z0))))), 0'(4(5(z0))), 4'(5(z0)))
0'(0(1(3(0(z0))))) → c15(0'(3(1(0(5(0(5(z0))))))), 3'(1(0(5(0(5(z0)))))), 0'(5(0(5(z0)))), 0'(5(z0)))
0'(0(2(0(1(z0))))) → c16(0'(0(0(3(2(1(z0)))))), 0'(0(3(2(1(z0))))), 0'(3(2(1(z0)))), 3'(2(1(z0))), 2'(1(z0)))
0'(1(1(3(4(z0))))) → c17(0'(5(4(1(3(1(z0)))))), 4'(1(3(1(z0)))), 3'(1(z0)))
0'(1(1(3(4(z0))))) → c18(4'(1(0(3(5(5(2(1(z0)))))))), 0'(3(5(5(2(1(z0)))))), 3'(5(5(2(1(z0))))), 2'(1(z0)))
0'(1(2(5(4(z0))))) → c19(3'(2(1(0(4(5(z0)))))), 2'(1(0(4(5(z0))))), 0'(4(5(z0))), 4'(5(z0)))
0'(5(5(0(1(z0))))) → c20(0'(5(5(5(1(0(2(z0))))))), 0'(2(z0)), 2'(z0))
0'(0(2(1(1(1(z0)))))) → c21(0'(4(1(0(2(1(z0)))))), 4'(1(0(2(1(z0))))), 0'(2(1(z0))), 2'(1(z0)))
0'(1(1(2(5(4(z0)))))) → c22(0'(2(3(1(4(5(1(z0))))))), 2'(3(1(4(5(1(z0)))))), 3'(1(4(5(1(z0))))), 4'(5(1(z0))))
0'(1(5(1(4(0(z0)))))) → c23(0'(5(1(4(2(1(0(5(z0)))))))), 4'(2(1(0(5(z0))))), 2'(1(0(5(z0)))), 0'(5(z0)))
0'(2(5(3(1(1(z0)))))) → c24(3'(0(2(1(3(5(1(z0))))))), 0'(2(1(3(5(1(z0)))))), 2'(1(3(5(1(z0))))), 3'(5(1(z0))))
0'(3(0(5(4(1(z0)))))) → c25(3'(2(1(0(4(5(0(z0))))))), 2'(1(0(4(5(0(z0)))))), 0'(4(5(0(z0)))), 4'(5(0(z0))), 0'(z0))
0'(5(5(3(3(4(z0)))))) → c26(3'(5(5(0(4(5(5(3(z0)))))))), 0'(4(5(5(3(z0))))), 4'(5(5(3(z0)))), 3'(z0))
0'(1(2(3(4(0(1(z0))))))) → c27(2'(0(4(5(1(3(1(0(z0)))))))), 0'(4(5(1(3(1(0(z0))))))), 4'(5(1(3(1(0(z0)))))), 3'(1(0(z0))), 0'(z0))
4'(0(1(z0))) → c28(3'(5(1(4(1(2(0(z0))))))), 4'(1(2(0(z0)))), 2'(0(z0)), 0'(z0))
4'(0(0(1(z0)))) → c29(4'(0(0(3(1(z0))))), 0'(0(3(1(z0)))), 0'(3(1(z0))), 3'(1(z0)))
4'(3(0(1(z0)))) → c30(3'(5(0(4(2(1(z0)))))), 0'(4(2(1(z0)))), 4'(2(1(z0))), 2'(1(z0)))
4'(3(0(1(z0)))) → c31(3'(1(4(2(5(5(2(0(z0)))))))), 4'(2(5(5(2(0(z0)))))), 2'(5(5(2(0(z0))))), 2'(0(z0)), 0'(z0))
4'(3(1(1(z0)))) → c32(4'(3(1(3(1(z0))))), 3'(1(3(1(z0)))), 3'(1(z0)))
4'(0(1(1(4(z0))))) → c33(4'(0(1(3(1(4(5(5(z0)))))))), 0'(1(3(1(4(5(5(z0))))))), 3'(1(4(5(5(z0))))), 4'(5(5(z0))))
4'(3(2(0(1(z0))))) → c34(3'(1(2(2(4(0(z0)))))), 2'(2(4(0(z0)))), 2'(4(0(z0))), 4'(0(z0)), 0'(z0))
4'(3(4(1(1(z0))))) → c35(3'(1(4(1(4(2(z0)))))), 4'(1(4(2(z0)))), 4'(2(z0)), 2'(z0))
4'(0(1(3(0(1(z0)))))) → c36(0'(3(1(4(1(0(3(z0))))))), 3'(1(4(1(0(3(z0)))))), 4'(1(0(3(z0)))), 0'(3(z0)), 3'(z0))
4'(0(3(4(1(1(z0)))))) → c37(0'(1(4(3(1(4(5(4(z0)))))))), 4'(3(1(4(5(4(z0)))))), 3'(1(4(5(4(z0))))), 4'(5(4(z0))), 4'(z0))
4'(2(0(5(1(1(z0)))))) → c38(3'(5(0(2(1(4(2(1(z0)))))))), 0'(2(1(4(2(1(z0)))))), 2'(1(4(2(1(z0))))), 4'(2(1(z0))), 2'(1(z0)))
4'(3(0(1(0(4(z0)))))) → c39(2'(0(4(5(1(3(0(4(z0)))))))), 0'(4(5(1(3(0(4(z0))))))), 4'(5(1(3(0(4(z0)))))), 3'(0(4(z0))), 0'(4(z0)), 4'(z0))
4'(0(3(2(0(0(1(z0))))))) → c40(0'(0(5(1(4(2(3(0(z0)))))))), 0'(5(1(4(2(3(0(z0))))))), 4'(2(3(0(z0)))), 2'(3(0(z0))), 3'(0(z0)), 0'(z0))
4'(3(0(5(0(1(4(z0))))))) → c41(0'(4(1(0(3(1(4(z0))))))), 4'(1(0(3(1(4(z0)))))), 0'(3(1(4(z0)))), 3'(1(4(z0))), 4'(z0))
2'(0(1(0(z0)))) → c42(2'(0(5(1(0(z0))))), 0'(5(1(0(z0)))), 0'(z0))
2'(0(1(1(z0)))) → c43(2'(0(2(1(3(1(z0)))))), 0'(2(1(3(1(z0))))), 2'(1(3(1(z0)))), 3'(1(z0)))
2'(3(1(1(z0)))) → c44(2'(3(1(4(1(z0))))), 3'(1(4(1(z0)))), 4'(1(z0)))
2'(3(1(1(z0)))) → c45(3'(1(3(2(1(z0))))), 3'(2(1(z0))), 2'(1(z0)))
2'(4(1(1(z0)))) → c46(2'(4(2(1(4(1(z0)))))), 4'(2(1(4(1(z0))))), 2'(1(4(1(z0)))), 4'(1(z0)))
2'(0(1(4(1(z0))))) → c47(0'(4(2(1(z0)))), 4'(2(1(z0))), 2'(1(z0)))
2'(2(3(1(1(z0))))) → c48(3'(2(2(1(4(1(z0)))))), 2'(2(1(4(1(z0))))), 2'(1(4(1(z0)))), 4'(1(z0)))
2'(3(4(1(1(z0))))) → c49(2'(1(3(5(4(1(z0)))))), 3'(5(4(1(z0)))), 4'(1(z0)))
2'(4(4(0(1(z0))))) → c50(4'(5(2(1(4(5(5(0(z0)))))))), 2'(1(4(5(5(0(z0)))))), 4'(5(5(0(z0)))), 0'(z0))
2'(0(4(4(1(1(z0)))))) → c51(4'(0(0(2(1(4(5(1(z0)))))))), 0'(0(2(1(4(5(1(z0))))))), 0'(2(1(4(5(1(z0)))))), 2'(1(4(5(1(z0))))), 4'(5(1(z0))))
2'(2(3(1(0(1(z0)))))) → c52(0'(2(5(2(1(3(1(z0))))))), 2'(5(2(1(3(1(z0)))))), 2'(1(3(1(z0)))), 3'(1(z0)))
2'(3(0(1(1(1(z0)))))) → c53(3'(1(4(1(0(2(5(1(z0)))))))), 4'(1(0(2(5(1(z0)))))), 0'(2(5(1(z0)))), 2'(5(1(z0))))
2'(3(2(3(0(1(z0)))))) → c54(2'(3(5(1(3(1(2(0(z0)))))))), 3'(5(1(3(1(2(0(z0))))))), 3'(1(2(0(z0)))), 2'(0(z0)), 0'(z0))
2'(3(4(1(0(1(z0)))))) → c55(3'(3(2(1(4(5(1(0(z0)))))))), 3'(2(1(4(5(1(0(z0))))))), 2'(1(4(5(1(0(z0)))))), 4'(5(1(0(z0)))), 0'(z0))
2'(3(4(5(4(1(1(z0))))))) → c56(2'(1(3(4(3(5(4(1(z0)))))))), 3'(4(3(5(4(1(z0)))))), 4'(3(5(4(1(z0))))), 3'(5(4(1(z0)))), 4'(1(z0)))
2'(4(0(2(1(0(1(z0))))))) → c57(0'(2(2(1(4(5(0(1(z0)))))))), 2'(2(1(4(5(0(1(z0))))))), 2'(1(4(5(0(1(z0)))))), 4'(5(0(1(z0)))), 0'(1(z0)))
2'(4(3(4(2(1(1(z0))))))) → c58(2'(5(1(2(4(4(3(1(z0)))))))), 2'(4(4(3(1(z0))))), 4'(4(3(1(z0)))), 4'(3(1(z0))), 3'(1(z0)))
2'(4(5(0(3(0(1(z0))))))) → c59(2'(0(0(4(3(2(5(1(z0)))))))), 0'(0(4(3(2(5(1(z0))))))), 0'(4(3(2(5(1(z0)))))), 4'(3(2(5(1(z0))))), 3'(2(5(1(z0)))), 2'(5(1(z0))))
3'(0(1(0(z0)))) → c60(3'(1(2(2(0(0(z0)))))), 2'(2(0(0(z0)))), 2'(0(0(z0))), 0'(0(z0)), 0'(z0))
3'(3(1(1(z0)))) → c61(3'(5(1(3(2(2(1(z0))))))), 3'(2(2(1(z0)))), 2'(2(1(z0))), 2'(1(z0)))
3'(4(0(1(z0)))) → c62(0'(3(1(4(1(z0))))), 3'(1(4(1(z0)))), 4'(1(z0)))
3'(4(1(1(z0)))) → c63(3'(4(1(3(1(z0))))), 4'(1(3(1(z0)))), 3'(1(z0)))
3'(4(5(4(z0)))) → c64(4'(1(4(5(3(z0))))), 4'(5(3(z0))), 3'(z0))
3'(0(4(0(1(z0))))) → c65(4'(0(3(1(2(2(0(z0))))))), 0'(3(1(2(2(0(z0)))))), 3'(1(2(2(0(z0))))), 2'(2(0(z0))), 2'(0(z0)), 0'(z0))
3'(2(3(1(1(z0))))) → c66(3'(5(1(3(2(1(z0)))))), 3'(2(1(z0))), 2'(1(z0)))
3'(3(0(1(0(z0))))) → c67(3'(2(5(2(1(3(0(0(z0)))))))), 2'(5(2(1(3(0(0(z0))))))), 2'(1(3(0(0(z0))))), 3'(0(0(z0))), 0'(0(z0)), 0'(z0))
3'(3(4(0(1(z0))))) → c68(3'(5(0(3(1(2(4(1(z0)))))))), 0'(3(1(2(4(1(z0)))))), 3'(1(2(4(1(z0))))), 2'(4(1(z0))), 4'(1(z0)))
3'(4(2(0(1(z0))))) → c69(0'(3(1(4(2(1(z0)))))), 3'(1(4(2(1(z0))))), 4'(2(1(z0))), 2'(1(z0)))
3'(4(3(0(1(z0))))) → c70(0'(3(1(3(5(4(z0)))))), 3'(1(3(5(4(z0))))), 3'(5(4(z0))), 4'(z0))
3'(0(1(4(1(1(z0)))))) → c71(3'(1(2(2(1(4(1(0(z0)))))))), 2'(2(1(4(1(0(z0)))))), 2'(1(4(1(0(z0))))), 4'(1(0(z0))), 0'(z0))
3'(0(5(2(5(4(z0)))))) → c72(4'(3(5(2(1(0(5(z0))))))), 3'(5(2(1(0(5(z0)))))), 2'(1(0(5(z0)))), 0'(5(z0)))
3'(3(0(2(5(0(z0)))))) → c73(3'(2(5(0(0(3(1(z0))))))), 2'(5(0(0(3(1(z0)))))), 0'(0(3(1(z0)))), 0'(3(1(z0))), 3'(1(z0)))
3'(3(1(4(0(0(z0)))))) → c74(4'(0(3(1(3(5(0(z0))))))), 0'(3(1(3(5(0(z0)))))), 3'(1(3(5(0(z0))))), 3'(5(0(z0))), 0'(z0))
3'(4(1(2(5(0(z0)))))) → c75(4'(4(5(0(3(2(1(z0))))))), 4'(5(0(3(2(1(z0)))))), 0'(3(2(1(z0)))), 3'(2(1(z0))), 2'(1(z0)))
3'(4(2(2(0(1(z0)))))) → c76(3'(2(2(3(1(4(5(0(z0)))))))), 2'(2(3(1(4(5(0(z0))))))), 2'(3(1(4(5(0(z0)))))), 3'(1(4(5(0(z0))))), 4'(5(0(z0))), 0'(z0))
3'(4(5(3(0(1(z0)))))) → c77(0'(3(2(5(3(4(z0)))))), 3'(2(5(3(4(z0))))), 2'(5(3(4(z0)))), 3'(4(z0)), 4'(z0))
3'(0(0(4(0(1(1(z0))))))) → c78(3'(2(1(0(0(0(4(1(z0)))))))), 2'(1(0(0(0(4(1(z0))))))), 0'(0(0(4(1(z0))))), 0'(0(4(1(z0)))), 0'(4(1(z0))), 4'(1(z0)))
3'(2(4(5(1(0(1(z0))))))) → c79(3'(5(2(1(4(1(0(z0))))))), 2'(1(4(1(0(z0))))), 4'(1(0(z0))), 0'(z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(0(z0))) → 0(2(1(0(z0))))
0(1(1(z0))) → 0(3(1(4(1(z0)))))
0(1(1(z0))) → 0(5(1(3(2(5(1(z0)))))))
0(1(1(z0))) → 3(5(5(1(0(2(1(z0)))))))
0(1(4(z0))) → 0(5(1(4(5(z0)))))
0(0(1(1(z0)))) → 2(0(5(1(4(1(0(z0)))))))
0(0(3(4(z0)))) → 0(3(2(1(4(5(5(0(z0))))))))
0(1(1(0(z0)))) → 2(1(0(3(1(0(z0))))))
0(1(1(4(z0)))) → 3(1(4(1(0(3(5(z0)))))))
0(1(3(0(z0)))) → 0(0(3(2(1(z0)))))
0(1(3(4(z0)))) → 3(1(4(2(5(0(5(z0)))))))
0(1(4(0(z0)))) → 0(5(0(4(1(3(1(z0)))))))
0(3(4(1(z0)))) → 4(3(0(3(1(z0)))))
0(0(0(1(1(z0))))) → 0(0(0(3(5(1(1(z0)))))))
0(0(0(3(4(z0))))) → 0(0(3(1(0(4(5(z0)))))))
0(0(1(3(0(z0))))) → 0(3(1(0(5(0(5(z0)))))))
0(0(2(0(1(z0))))) → 0(0(0(3(2(1(z0))))))
0(1(1(3(4(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(3(4(z0))))) → 4(1(0(3(5(5(2(1(z0))))))))
0(1(2(5(4(z0))))) → 3(2(1(0(4(5(z0))))))
0(5(5(0(1(z0))))) → 0(5(5(5(1(0(2(z0)))))))
0(0(2(1(1(1(z0)))))) → 5(1(0(4(1(0(2(1(z0))))))))
0(1(1(2(5(4(z0)))))) → 0(2(3(1(4(5(1(z0)))))))
0(1(5(1(4(0(z0)))))) → 0(5(1(4(2(1(0(5(z0))))))))
0(2(5(3(1(1(z0)))))) → 3(0(2(1(3(5(1(z0)))))))
0(3(0(5(4(1(z0)))))) → 3(2(1(0(4(5(0(z0)))))))
0(5(5(3(3(4(z0)))))) → 3(5(5(0(4(5(5(3(z0))))))))
0(1(2(3(4(0(1(z0))))))) → 2(0(4(5(1(3(1(0(z0))))))))
4(0(1(z0))) → 3(5(1(4(1(2(0(z0)))))))
4(0(0(1(z0)))) → 4(0(0(3(1(z0)))))
4(3(0(1(z0)))) → 3(5(0(4(2(1(z0))))))
4(3(0(1(z0)))) → 3(1(4(2(5(5(2(0(z0))))))))
4(3(1(1(z0)))) → 4(3(1(3(1(z0)))))
4(0(1(1(4(z0))))) → 4(0(1(3(1(4(5(5(z0))))))))
4(3(2(0(1(z0))))) → 3(1(2(2(4(0(z0))))))
4(3(4(1(1(z0))))) → 3(1(4(1(4(2(z0))))))
4(0(1(3(0(1(z0)))))) → 0(3(1(4(1(0(3(z0)))))))
4(0(3(4(1(1(z0)))))) → 0(1(4(3(1(4(5(4(z0))))))))
4(2(0(5(1(1(z0)))))) → 3(5(0(2(1(4(2(1(z0))))))))
4(3(0(1(0(4(z0)))))) → 2(0(4(5(1(3(0(4(z0))))))))
4(0(3(2(0(0(1(z0))))))) → 0(0(5(1(4(2(3(0(z0))))))))
4(3(0(5(0(1(4(z0))))))) → 5(0(4(1(0(3(1(4(z0))))))))
2(0(1(0(z0)))) → 2(0(5(1(0(z0)))))
2(0(1(1(z0)))) → 2(0(2(1(3(1(z0))))))
2(3(1(1(z0)))) → 2(3(1(4(1(z0)))))
2(3(1(1(z0)))) → 3(1(3(2(1(z0)))))
2(4(1(1(z0)))) → 2(4(2(1(4(1(z0))))))
2(0(1(4(1(z0))))) → 5(5(1(0(4(2(1(z0)))))))
2(2(3(1(1(z0))))) → 3(2(2(1(4(1(z0))))))
2(3(4(1(1(z0))))) → 2(1(3(5(4(1(z0))))))
2(4(4(0(1(z0))))) → 4(5(2(1(4(5(5(0(z0))))))))
2(0(4(4(1(1(z0)))))) → 4(0(0(2(1(4(5(1(z0))))))))
2(2(3(1(0(1(z0)))))) → 0(2(5(2(1(3(1(z0)))))))
2(3(0(1(1(1(z0)))))) → 3(1(4(1(0(2(5(1(z0))))))))
2(3(2(3(0(1(z0)))))) → 2(3(5(1(3(1(2(0(z0))))))))
2(3(4(1(0(1(z0)))))) → 3(3(2(1(4(5(1(0(z0))))))))
2(3(4(5(4(1(1(z0))))))) → 2(1(3(4(3(5(4(1(z0))))))))
2(4(0(2(1(0(1(z0))))))) → 0(2(2(1(4(5(0(1(z0))))))))
2(4(3(4(2(1(1(z0))))))) → 2(5(1(2(4(4(3(1(z0))))))))
2(4(5(0(3(0(1(z0))))))) → 2(0(0(4(3(2(5(1(z0))))))))
3(0(1(0(z0)))) → 3(1(2(2(0(0(z0))))))
3(3(1(1(z0)))) → 5(3(5(1(3(2(2(1(z0))))))))
3(4(0(1(z0)))) → 0(3(1(4(1(z0)))))
3(4(1(1(z0)))) → 3(4(1(3(1(z0)))))
3(4(5(4(z0)))) → 5(1(4(1(4(5(3(z0)))))))
3(0(4(0(1(z0))))) → 4(0(3(1(2(2(0(z0)))))))
3(2(3(1(1(z0))))) → 3(5(1(3(2(1(z0))))))
3(3(0(1(0(z0))))) → 3(2(5(2(1(3(0(0(z0))))))))
3(3(4(0(1(z0))))) → 3(5(0(3(1(2(4(1(z0))))))))
3(4(2(0(1(z0))))) → 0(3(1(4(2(1(z0))))))
3(4(3(0(1(z0))))) → 0(3(1(3(5(4(z0))))))
3(0(1(4(1(1(z0)))))) → 3(1(2(2(1(4(1(0(z0))))))))
3(0(5(2(5(4(z0)))))) → 4(3(5(2(1(0(5(z0)))))))
3(3(0(2(5(0(z0)))))) → 3(2(5(0(0(3(1(z0)))))))
3(3(1(4(0(0(z0)))))) → 4(0(3(1(3(5(0(z0)))))))
3(4(1(2(5(0(z0)))))) → 4(4(5(0(3(2(1(z0)))))))
3(4(2(2(0(1(z0)))))) → 3(2(2(3(1(4(5(0(z0))))))))
3(4(5(3(0(1(z0)))))) → 5(1(0(3(2(5(3(4(z0))))))))
3(0(0(4(0(1(1(z0))))))) → 3(2(1(0(0(0(4(1(z0))))))))
3(2(4(5(1(0(1(z0))))))) → 1(3(5(2(1(4(1(0(z0))))))))
Tuples:
0'(1(1(z0))) → c1(0'(3(1(4(1(z0))))), 3'(1(4(1(z0)))), 4'(1(z0)))
0'(1(1(z0))) → c2(0'(5(1(3(2(5(1(z0))))))), 3'(2(5(1(z0)))), 2'(5(1(z0))))
0'(1(1(z0))) → c3(3'(5(5(1(0(2(1(z0))))))), 0'(2(1(z0))), 2'(1(z0)))
S tuples:
0'(1(1(z0))) → c1(0'(3(1(4(1(z0))))), 3'(1(4(1(z0)))), 4'(1(z0)))
0'(1(1(z0))) → c2(0'(5(1(3(2(5(1(z0))))))), 3'(2(5(1(z0)))), 2'(5(1(z0))))
0'(1(1(z0))) → c3(3'(5(5(1(0(2(1(z0))))))), 0'(2(1(z0))), 2'(1(z0)))
K tuples:none
Defined Rule Symbols:
0, 4, 2, 3
Defined Pair Symbols:
0'
Compound Symbols:
c1, c2, c3
(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)
Removed 3 of 3 dangling nodes:
0'(1(1(z0))) → c1(0'(3(1(4(1(z0))))), 3'(1(4(1(z0)))), 4'(1(z0)))
0'(1(1(z0))) → c2(0'(5(1(3(2(5(1(z0))))))), 3'(2(5(1(z0)))), 2'(5(1(z0))))
0'(1(1(z0))) → c3(3'(5(5(1(0(2(1(z0))))))), 0'(2(1(z0))), 2'(1(z0)))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(0(z0))) → 0(2(1(0(z0))))
0(1(1(z0))) → 0(3(1(4(1(z0)))))
0(1(1(z0))) → 0(5(1(3(2(5(1(z0)))))))
0(1(1(z0))) → 3(5(5(1(0(2(1(z0)))))))
0(1(4(z0))) → 0(5(1(4(5(z0)))))
0(0(1(1(z0)))) → 2(0(5(1(4(1(0(z0)))))))
0(0(3(4(z0)))) → 0(3(2(1(4(5(5(0(z0))))))))
0(1(1(0(z0)))) → 2(1(0(3(1(0(z0))))))
0(1(1(4(z0)))) → 3(1(4(1(0(3(5(z0)))))))
0(1(3(0(z0)))) → 0(0(3(2(1(z0)))))
0(1(3(4(z0)))) → 3(1(4(2(5(0(5(z0)))))))
0(1(4(0(z0)))) → 0(5(0(4(1(3(1(z0)))))))
0(3(4(1(z0)))) → 4(3(0(3(1(z0)))))
0(0(0(1(1(z0))))) → 0(0(0(3(5(1(1(z0)))))))
0(0(0(3(4(z0))))) → 0(0(3(1(0(4(5(z0)))))))
0(0(1(3(0(z0))))) → 0(3(1(0(5(0(5(z0)))))))
0(0(2(0(1(z0))))) → 0(0(0(3(2(1(z0))))))
0(1(1(3(4(z0))))) → 0(5(4(1(3(1(z0))))))
0(1(1(3(4(z0))))) → 4(1(0(3(5(5(2(1(z0))))))))
0(1(2(5(4(z0))))) → 3(2(1(0(4(5(z0))))))
0(5(5(0(1(z0))))) → 0(5(5(5(1(0(2(z0)))))))
0(0(2(1(1(1(z0)))))) → 5(1(0(4(1(0(2(1(z0))))))))
0(1(1(2(5(4(z0)))))) → 0(2(3(1(4(5(1(z0)))))))
0(1(5(1(4(0(z0)))))) → 0(5(1(4(2(1(0(5(z0))))))))
0(2(5(3(1(1(z0)))))) → 3(0(2(1(3(5(1(z0)))))))
0(3(0(5(4(1(z0)))))) → 3(2(1(0(4(5(0(z0)))))))
0(5(5(3(3(4(z0)))))) → 3(5(5(0(4(5(5(3(z0))))))))
0(1(2(3(4(0(1(z0))))))) → 2(0(4(5(1(3(1(0(z0))))))))
4(0(1(z0))) → 3(5(1(4(1(2(0(z0)))))))
4(0(0(1(z0)))) → 4(0(0(3(1(z0)))))
4(3(0(1(z0)))) → 3(5(0(4(2(1(z0))))))
4(3(0(1(z0)))) → 3(1(4(2(5(5(2(0(z0))))))))
4(3(1(1(z0)))) → 4(3(1(3(1(z0)))))
4(0(1(1(4(z0))))) → 4(0(1(3(1(4(5(5(z0))))))))
4(3(2(0(1(z0))))) → 3(1(2(2(4(0(z0))))))
4(3(4(1(1(z0))))) → 3(1(4(1(4(2(z0))))))
4(0(1(3(0(1(z0)))))) → 0(3(1(4(1(0(3(z0)))))))
4(0(3(4(1(1(z0)))))) → 0(1(4(3(1(4(5(4(z0))))))))
4(2(0(5(1(1(z0)))))) → 3(5(0(2(1(4(2(1(z0))))))))
4(3(0(1(0(4(z0)))))) → 2(0(4(5(1(3(0(4(z0))))))))
4(0(3(2(0(0(1(z0))))))) → 0(0(5(1(4(2(3(0(z0))))))))
4(3(0(5(0(1(4(z0))))))) → 5(0(4(1(0(3(1(4(z0))))))))
2(0(1(0(z0)))) → 2(0(5(1(0(z0)))))
2(0(1(1(z0)))) → 2(0(2(1(3(1(z0))))))
2(3(1(1(z0)))) → 2(3(1(4(1(z0)))))
2(3(1(1(z0)))) → 3(1(3(2(1(z0)))))
2(4(1(1(z0)))) → 2(4(2(1(4(1(z0))))))
2(0(1(4(1(z0))))) → 5(5(1(0(4(2(1(z0)))))))
2(2(3(1(1(z0))))) → 3(2(2(1(4(1(z0))))))
2(3(4(1(1(z0))))) → 2(1(3(5(4(1(z0))))))
2(4(4(0(1(z0))))) → 4(5(2(1(4(5(5(0(z0))))))))
2(0(4(4(1(1(z0)))))) → 4(0(0(2(1(4(5(1(z0))))))))
2(2(3(1(0(1(z0)))))) → 0(2(5(2(1(3(1(z0)))))))
2(3(0(1(1(1(z0)))))) → 3(1(4(1(0(2(5(1(z0))))))))
2(3(2(3(0(1(z0)))))) → 2(3(5(1(3(1(2(0(z0))))))))
2(3(4(1(0(1(z0)))))) → 3(3(2(1(4(5(1(0(z0))))))))
2(3(4(5(4(1(1(z0))))))) → 2(1(3(4(3(5(4(1(z0))))))))
2(4(0(2(1(0(1(z0))))))) → 0(2(2(1(4(5(0(1(z0))))))))
2(4(3(4(2(1(1(z0))))))) → 2(5(1(2(4(4(3(1(z0))))))))
2(4(5(0(3(0(1(z0))))))) → 2(0(0(4(3(2(5(1(z0))))))))
3(0(1(0(z0)))) → 3(1(2(2(0(0(z0))))))
3(3(1(1(z0)))) → 5(3(5(1(3(2(2(1(z0))))))))
3(4(0(1(z0)))) → 0(3(1(4(1(z0)))))
3(4(1(1(z0)))) → 3(4(1(3(1(z0)))))
3(4(5(4(z0)))) → 5(1(4(1(4(5(3(z0)))))))
3(0(4(0(1(z0))))) → 4(0(3(1(2(2(0(z0)))))))
3(2(3(1(1(z0))))) → 3(5(1(3(2(1(z0))))))
3(3(0(1(0(z0))))) → 3(2(5(2(1(3(0(0(z0))))))))
3(3(4(0(1(z0))))) → 3(5(0(3(1(2(4(1(z0))))))))
3(4(2(0(1(z0))))) → 0(3(1(4(2(1(z0))))))
3(4(3(0(1(z0))))) → 0(3(1(3(5(4(z0))))))
3(0(1(4(1(1(z0)))))) → 3(1(2(2(1(4(1(0(z0))))))))
3(0(5(2(5(4(z0)))))) → 4(3(5(2(1(0(5(z0)))))))
3(3(0(2(5(0(z0)))))) → 3(2(5(0(0(3(1(z0)))))))
3(3(1(4(0(0(z0)))))) → 4(0(3(1(3(5(0(z0)))))))
3(4(1(2(5(0(z0)))))) → 4(4(5(0(3(2(1(z0)))))))
3(4(2(2(0(1(z0)))))) → 3(2(2(3(1(4(5(0(z0))))))))
3(4(5(3(0(1(z0)))))) → 5(1(0(3(2(5(3(4(z0))))))))
3(0(0(4(0(1(1(z0))))))) → 3(2(1(0(0(0(4(1(z0))))))))
3(2(4(5(1(0(1(z0))))))) → 1(3(5(2(1(4(1(0(z0))))))))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
0, 4, 2, 3
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))